A software system contains a functionally closed set of procedures. In order to ensure correct implementation of the software system, it is desirable to determine a software contract, i.e., elements and functional specifications of external interfaces of the software system, and carry out conformance testing of the software contract implementation. Since the elements of the software contract are procedures, it is in fact Application Programming Interface (API) testing.
A kernel of an Operating System (OS) comprises API. For example, a Support Operating System (SOS) is a real-time OS for a Digital Multiplexing Switch (DMS) for a communication system. SOS comprises a plurality of processes for supporting the operation of DMS. The lowest layer of SOS is SOS kernel. The SOS kernel allocates resources to the processes running under SOS. The SOS kernel also provides communication among these processes. The SOS kernel also creates, controls and removes these processes.
SOS supports more than 25 million lines of code for applications and utilities. Thus, it is critical that user procedure interfaces of the SOS kernel be stable and reliable for correct performances of the DMS switch. The SOS kernel consists of over 17,000 procedures or over 230,000 lines of source code. Thus, it is very complicated and time consuming processes to generate a system for verifying such complex procedure interfaces. There existed no automatic or semi-automatic mechanisms to aid such generation of a verification system.
At the same time, SOS continuously evolves. Also, SOS is often ported to new hardware and software platforms. While more than 75% of the kernel procedures are machine-independent, the remainder of the kernel procedures are very machine dependent. The remainder describes particularity of memory, inter-processor communication and communication with peripheral devices. Accordingly, when SOS evolves or SOS is ported to a new platform, the SOS kernel and its procedure interfaces are also modified. Thus, the verification system for the procedure interfaces of the SOS kernel also needs to be modified. However, there existed no automatic or semi-automatic modifying mechanisms to aid such modifications.
There are some systems proposed for building a verification process. One of such systems is Interactive Tree and Tabular Combined Notation (TTCN) Editor and eXecutor (ITEX). ITEX is a test environment for communicating systems. It includes a TTCN and Abstract Syntax Notation.1 (ASN.1) analysis and design tool, a test simulator and support for generation of complete Executable Test Suites (ETS). In accordance with ITEX, a Test Suite is made up of Test Cases in form of tables. ITEX provides a set of highly integrated tools for development and maintenance of Abstract Test Suites (ATS) written in TTCN. ITEX supports phases of the test suite development including Test Case Generation, Editing, Verification, Validation and Execution. This toolset is integrated with the Specification Description Language (SDL) Design Tool (SDT), which is an environment for design of SDL specifications. Test suites described with TTCN can be transformed to the form that allows testing both implementation in some programming language and specification in SDL. However, this approach is unsuitable for API testing. TTCN does not permit declaration of pointers and other software entities that do not have textural (literal) representation. A major limitation of SDL-like specifications is their explicit form. This means that it is easy to build models and prototypes based on them but it is very difficult to develop a system of constraints that define the union of all possible implementations.
Another example is the Algebraic Design Language (ADL)/ADL2. From formal specifications, ADL generates test oracles and skeletons for building test drivers and documentation. ADL uses not one of the popular specification languages but extensions of C and C++ languages. There are ideas on extensions of Java and other object-oriented languages aimed at developing software in “Design-by-Contract” fashion. However, despite the obvious advantages of better acceptance of such languages in the software engineering community, the concept, not to mention the common notation, is still far in the future. ADL has a limited range of API classes for which it can provides means for specifications and automatic test generation. ADL provides adequate tools for test generation automation only for procedures whose parameters allow independent enumeration and allows testing procedures one by one. This means that ADL omits procedures with dependent parameters, procedures that require testing in a group, e.g., “open-close”, or those that require testing in parallel mode, e.g., “lock-unlock”, or “send-receive”.
Another example is formal derivation of Finite State Machines (FSM) for class testing proposed by L. Murray, D. Carrington, I. MacColl, J. McDonald and P. Strooper in “Formal Derivation of Finite State Machines for Class Testing”, in Jonatthan P. Bowen, Andreas Fett, Michael G. Hinchey (eds.) ZUM'98: The Z Formal Specification Notation. 11-th International Conference of Z Users, Berlin, Germany, September 1998, Proceeding, Lecture Notes in Computer Science, v. 1493, pp. 42-59. This work is at the research stage. The authors propose a scheme for organization of procedure group testing using Object-Z as specification language and C++ as programming language. The task of this work is stated to build test suites to verify conformance of the implementation to the specification using formal specifications of the methods for a class. As a test coverage criterion, the union of two criteria is used: to cover all equivalency classes that represent the areas obtained as a result of partition analysis, and then, to check results on or near the boundaries. However, the authors of this work do not try to solve the problem of complete automation of test generation. Nor do they attempt to support any elements of the preparation phase with tools. Partition and boundary analysis is done manually according to the methodology proposed by the authors. In a similar way, they build the specification of oracles. Oracles, once compiled into C++, call target procedures and verify the conformance of the results to the specifications. This testing scheme is a framework that dynamically generates test sequences of procedure calls. The framework is controlled by the FSM description which represents an abstraction of a state transition graph of the test class. The authors describe the methodology of building specifications for the classes of states and transitions between them while considering the problem of exclusion of inaccessible states.
This approach needs the full description of the FSM that models the states of the system under test. The theoretical weakness of this approach is that it does not try to come up with a formal methodology to build transformation specifications. It is obvious that serious problems will be encountered when attempting to apply this approach to specifications of real-life complexity. In practical sense, it is clear that the process of test derivation from the specifications is mostly manual activity which limits its applicability to industrial software.
The development of verification system is a labour-intensive process. The total size of a verification system is often similar to the size of the software under test.
Currently, the most commonly used approach to the verification system development is the manual development. There are some tools that can generate some elements of a verification system for the most simple cases of the test parameter set generation, namely, for the case of the manually written list of the test parameter sets in literal form. However, this approach can not be used if some parameter could not be written in literal form. For example, a UNIX file descriptor is returned by operating system as a result of the system call “open file”, and can not be written in literal form. This approach also can not be used for testing of the procedure sequence when the out-parameter of some procedure is used as the in-parameter of the another procedure.
It is therefore desirable to provide means to decrease the efforts of the verification system development and to increase its reliability.